(set-logic QF_BV)
(set-info :source |
Number of leading zeros nlz(x) algorithm, binary search 
From the book "Hacker's delight" by Henry S. Warren, Jr., page 78
We cross-check it with an obvious method of counting leading zeros:

s = 0;
for (i = BW - 1; i >= 0; i--)
  if (x & (1 << i))
    break;
  else
    s++;

Contributed by Robert Brummayer (robert.brummayer@gmail.com)
|)
(set-info :smt-lib-version 2.0)
(set-info :category "crafted")
(set-info :status unsat)
(declare-fun x () (_ BitVec 128))
(assert (let ((?v_0 ((_ zero_extend 121) (_ bv64 7)))) (let ((?v_9 (= (_ bv1 1) (ite (= (bvlshr x ?v_0) (_ bv0 128)) (_ bv1 1) (_ bv0 1))))) (let ((?v_10 (ite ?v_9 (bvadd (_ bv1 128) (_ bv64 128)) (_ bv1 128))) (?v_1 (ite ?v_9 (bvshl x ?v_0) x)) (?v_22 ((_ zero_extend 121) (_ bv96 7)))) (let ((?v_8 (= (_ bv1 1) (ite (= (bvlshr ?v_1 ?v_22) (_ bv0 128)) (_ bv1 1) (_ bv0 1))))) (let ((?v_11 (ite ?v_8 (bvadd ?v_10 (_ bv32 128)) ?v_10)) (?v_23 ((_ zero_extend 121) (_ bv32 7)))) (let ((?v_2 (ite ?v_8 (bvshl ?v_1 ?v_23) ?v_1)) (?v_21 ((_ zero_extend 121) (_ bv112 7)))) (let ((?v_7 (= (_ bv1 1) (ite (= (bvlshr ?v_2 ?v_21) (_ bv0 128)) (_ bv1 1) (_ bv0 1))))) (let ((?v_12 (ite ?v_7 (bvadd ?v_11 (_ bv16 128)) ?v_11)) (?v_24 ((_ zero_extend 121) (_ bv16 7)))) (let ((?v_3 (ite ?v_7 (bvshl ?v_2 ?v_24) ?v_2)) (?v_20 ((_ zero_extend 121) (_ bv120 7)))) (let ((?v_6 (= (_ bv1 1) (ite (= (bvlshr ?v_3 ?v_20) (_ bv0 128)) (_ bv1 1) (_ bv0 1))))) (let ((?v_13 (ite ?v_6 (bvadd ?v_12 (_ bv8 128)) ?v_12)) (?v_25 ((_ zero_extend 121) (_ bv8 7)))) (let ((?v_4 (ite ?v_6 (bvshl ?v_3 ?v_25) ?v_3)) (?v_19 ((_ zero_extend 121) (_ bv124 7)))) (let ((?v_5 (= (_ bv1 1) (ite (= (bvlshr ?v_4 ?v_19) (_ bv0 128)) (_ bv1 1) (_ bv0 1))))) (let ((?v_14 (ite ?v_5 (bvadd ?v_13 (_ bv4 128)) ?v_13)) (?v_26 ((_ zero_extend 121) (_ bv4 7)))) (let ((?v_16 (ite ?v_5 (bvshl ?v_4 ?v_26) ?v_4)) (?v_18 ((_ zero_extend 121) (_ bv126 7)))) (let ((?v_15 (= (_ bv1 1) (ite (= (bvlshr ?v_16 ?v_18) (_ bv0 128)) (_ bv1 1) (_ bv0 1)))) (?v_27 ((_ zero_extend 121) (_ bv2 7))) (?v_17 ((_ zero_extend 121) (_ bv127 7)))) (let ((?v_281 (ite (= (bvand x (bvshl (_ bv1 128) ?v_17)) (_ bv0 128)) (_ bv1 1) (_ bv0 1)))) (let ((?v_282 (bvor (_ bv0 1) (bvnot ?v_281)))) (let ((?v_283 (ite (= (_ bv1 1) ?v_281) (ite (= (_ bv1 1) ?v_282) (_ bv0 128) (bvadd (_ bv0 128) (_ bv1 128))) (_ bv0 128))) (?v_279 (ite (= (bvand x (bvshl (_ bv1 128) ?v_18)) (_ bv0 128)) (_ bv1 1) (_ bv0 1)))) (let ((?v_280 (bvor ?v_282 (bvnot ?v_279)))) (let ((?v_284 (ite (= (_ bv1 1) ?v_279) (ite (= (_ bv1 1) ?v_280) ?v_283 (bvadd ?v_283 (_ bv1 128))) ?v_283)) (?v_277 (ite (= (bvand x (bvshl (_ bv1 128) ((_ zero_extend 121) (_ bv125 7)))) (_ bv0 128)) (_ bv1 1) (_ bv0 1)))) (let ((?v_278 (bvor ?v_280 (bvnot ?v_277)))) (let ((?v_285 (ite (= (_ bv1 1) ?v_277) (ite (= (_ bv1 1) ?v_278) ?v_284 (bvadd ?v_284 (_ bv1 128))) ?v_284)) (?v_275 (ite (= (bvand x (bvshl (_ bv1 128) ?v_19)) (_ bv0 128)) (_ bv1 1) (_ bv0 1)))) (let ((?v_276 (bvor ?v_278 (bvnot ?v_275)))) (let ((?v_286 (ite (= (_ bv1 1) ?v_275) (ite (= (_ bv1 1) ?v_276) ?v_285 (bvadd ?v_285 (_ bv1 128))) ?v_285)) (?v_273 (ite (= (bvand x (bvshl (_ bv1 128) ((_ zero_extend 121) (_ bv123 7)))) (_ bv0 128)) (_ bv1 1) (_ bv0 1)))) (let ((?v_274 (bvor ?v_276 (bvnot ?v_273)))) (let ((?v_287 (ite (= (_ bv1 1) ?v_273) (ite (= (_ bv1 1) ?v_274) ?v_286 (bvadd ?v_286 (_ bv1 128))) ?v_286)) (?v_271 (ite (= (bvand x (bvshl (_ bv1 128) ((_ zero_extend 121) (_ bv122 7)))) (_ bv0 128)) (_ bv1 1) (_ bv0 1)))) (let ((?v_272 (bvor ?v_274 (bvnot ?v_271)))) (let ((?v_288 (ite (= (_ bv1 1) ?v_271) (ite (= (_ bv1 1) ?v_272) ?v_287 (bvadd ?v_287 (_ bv1 128))) ?v_287)) (?v_269 (ite (= (bvand x (bvshl (_ bv1 128) ((_ zero_extend 121) (_ bv121 7)))) (_ bv0 128)) (_ bv1 1) (_ bv0 1)))) (let ((?v_270 (bvor ?v_272 (bvnot ?v_269)))) (let ((?v_289 (ite (= (_ bv1 1) ?v_269) (ite (= (_ bv1 1) ?v_270) ?v_288 (bvadd ?v_288 (_ bv1 128))) ?v_288)) (?v_267 (ite (= (bvand x (bvshl (_ bv1 128) ?v_20)) (_ bv0 128)) (_ bv1 1) (_ bv0 1)))) (let ((?v_268 (bvor ?v_270 (bvnot ?v_267)))) (let ((?v_290 (ite (= (_ bv1 1) ?v_267) (ite (= (_ bv1 1) ?v_268) ?v_289 (bvadd ?v_289 (_ bv1 128))) ?v_289)) (?v_265 (ite (= (bvand x (bvshl (_ bv1 128) ((_ zero_extend 121) (_ bv119 7)))) (_ bv0 128)) (_ bv1 1) (_ bv0 1)))) (let ((?v_266 (bvor ?v_268 (bvnot ?v_265)))) (let ((?v_291 (ite (= (_ bv1 1) ?v_265) (ite (= (_ bv1 1) ?v_266) ?v_290 (bvadd ?v_290 (_ bv1 128))) ?v_290)) (?v_263 (ite (= (bvand x (bvshl (_ bv1 128) ((_ zero_extend 121) (_ bv118 7)))) (_ bv0 128)) (_ bv1 1) (_ bv0 1)))) (let ((?v_264 (bvor ?v_266 (bvnot ?v_263)))) (let ((?v_292 (ite (= (_ bv1 1) ?v_263) (ite (= (_ bv1 1) ?v_264) ?v_291 (bvadd ?v_291 (_ bv1 128))) ?v_291)) (?v_261 (ite (= (bvand x (bvshl (_ bv1 128) ((_ zero_extend 121) (_ bv117 7)))) (_ bv0 128)) (_ bv1 1) (_ bv0 1)))) (let ((?v_262 (bvor ?v_264 (bvnot ?v_261)))) (let ((?v_293 (ite (= (_ bv1 1) ?v_261) (ite (= (_ bv1 1) ?v_262) ?v_292 (bvadd ?v_292 (_ bv1 128))) ?v_292)) (?v_259 (ite (= (bvand x (bvshl (_ bv1 128) ((_ zero_extend 121) (_ bv116 7)))) (_ bv0 128)) (_ bv1 1) (_ bv0 1)))) (let ((?v_260 (bvor ?v_262 (bvnot ?v_259)))) (let ((?v_294 (ite (= (_ bv1 1) ?v_259) (ite (= (_ bv1 1) ?v_260) ?v_293 (bvadd ?v_293 (_ bv1 128))) ?v_293)) (?v_257 (ite (= (bvand x (bvshl (_ bv1 128) ((_ zero_extend 121) (_ bv115 7)))) (_ bv0 128)) (_ bv1 1) (_ bv0 1)))) (let ((?v_258 (bvor ?v_260 (bvnot ?v_257)))) (let ((?v_295 (ite (= (_ bv1 1) ?v_257) (ite (= (_ bv1 1) ?v_258) ?v_294 (bvadd ?v_294 (_ bv1 128))) ?v_294)) (?v_255 (ite (= (bvand x (bvshl (_ bv1 128) ((_ zero_extend 121) (_ bv114 7)))) (_ bv0 128)) (_ bv1 1) (_ bv0 1)))) (let ((?v_256 (bvor ?v_258 (bvnot ?v_255)))) (let ((?v_296 (ite (= (_ bv1 1) ?v_255) (ite (= (_ bv1 1) ?v_256) ?v_295 (bvadd ?v_295 (_ bv1 128))) ?v_295)) (?v_253 (ite (= (bvand x (bvshl (_ bv1 128) ((_ zero_extend 121) (_ bv113 7)))) (_ bv0 128)) (_ bv1 1) (_ bv0 1)))) (let ((?v_254 (bvor ?v_256 (bvnot ?v_253)))) (let ((?v_297 (ite (= (_ bv1 1) ?v_253) (ite (= (_ bv1 1) ?v_254) ?v_296 (bvadd ?v_296 (_ bv1 128))) ?v_296)) (?v_251 (ite (= (bvand x (bvshl (_ bv1 128) ?v_21)) (_ bv0 128)) (_ bv1 1) (_ bv0 1)))) (let ((?v_252 (bvor ?v_254 (bvnot ?v_251)))) (let ((?v_298 (ite (= (_ bv1 1) ?v_251) (ite (= (_ bv1 1) ?v_252) ?v_297 (bvadd ?v_297 (_ bv1 128))) ?v_297)) (?v_249 (ite (= (bvand x (bvshl (_ bv1 128) ((_ zero_extend 121) (_ bv111 7)))) (_ bv0 128)) (_ bv1 1) (_ bv0 1)))) (let ((?v_250 (bvor ?v_252 (bvnot ?v_249)))) (let ((?v_299 (ite (= (_ bv1 1) ?v_249) (ite (= (_ bv1 1) ?v_250) ?v_298 (bvadd ?v_298 (_ bv1 128))) ?v_298)) (?v_247 (ite (= (bvand x (bvshl (_ bv1 128) ((_ zero_extend 121) (_ bv110 7)))) (_ bv0 128)) (_ bv1 1) (_ bv0 1)))) (let ((?v_248 (bvor ?v_250 (bvnot ?v_247)))) (let ((?v_300 (ite (= (_ bv1 1) ?v_247) (ite (= (_ bv1 1) ?v_248) ?v_299 (bvadd ?v_299 (_ bv1 128))) ?v_299)) (?v_245 (ite (= (bvand x (bvshl (_ bv1 128) ((_ zero_extend 121) (_ bv109 7)))) (_ bv0 128)) (_ bv1 1) (_ bv0 1)))) (let ((?v_246 (bvor ?v_248 (bvnot ?v_245)))) (let ((?v_301 (ite (= (_ bv1 1) ?v_245) (ite (= (_ bv1 1) ?v_246) ?v_300 (bvadd ?v_300 (_ bv1 128))) ?v_300)) (?v_243 (ite (= (bvand x (bvshl (_ bv1 128) ((_ zero_extend 121) (_ bv108 7)))) (_ bv0 128)) (_ bv1 1) (_ bv0 1)))) (let ((?v_244 (bvor ?v_246 (bvnot ?v_243)))) (let ((?v_302 (ite (= (_ bv1 1) ?v_243) (ite (= (_ bv1 1) ?v_244) ?v_301 (bvadd ?v_301 (_ bv1 128))) ?v_301)) (?v_241 (ite (= (bvand x (bvshl (_ bv1 128) ((_ zero_extend 121) (_ bv107 7)))) (_ bv0 128)) (_ bv1 1) (_ bv0 1)))) (let ((?v_242 (bvor ?v_244 (bvnot ?v_241)))) (let ((?v_303 (ite (= (_ bv1 1) ?v_241) (ite (= (_ bv1 1) ?v_242) ?v_302 (bvadd ?v_302 (_ bv1 128))) ?v_302)) (?v_239 (ite (= (bvand x (bvshl (_ bv1 128) ((_ zero_extend 121) (_ bv106 7)))) (_ bv0 128)) (_ bv1 1) (_ bv0 1)))) (let ((?v_240 (bvor ?v_242 (bvnot ?v_239)))) (let ((?v_304 (ite (= (_ bv1 1) ?v_239) (ite (= (_ bv1 1) ?v_240) ?v_303 (bvadd ?v_303 (_ bv1 128))) ?v_303)) (?v_237 (ite (= (bvand x (bvshl (_ bv1 128) ((_ zero_extend 121) (_ bv105 7)))) (_ bv0 128)) (_ bv1 1) (_ bv0 1)))) (let ((?v_238 (bvor ?v_240 (bvnot ?v_237)))) (let ((?v_305 (ite (= (_ bv1 1) ?v_237) (ite (= (_ bv1 1) ?v_238) ?v_304 (bvadd ?v_304 (_ bv1 128))) ?v_304)) (?v_235 (ite (= (bvand x (bvshl (_ bv1 128) ((_ zero_extend 121) (_ bv104 7)))) (_ bv0 128)) (_ bv1 1) (_ bv0 1)))) (let ((?v_236 (bvor ?v_238 (bvnot ?v_235)))) (let ((?v_306 (ite (= (_ bv1 1) ?v_235) (ite (= (_ bv1 1) ?v_236) ?v_305 (bvadd ?v_305 (_ bv1 128))) ?v_305)) (?v_233 (ite (= (bvand x (bvshl (_ bv1 128) ((_ zero_extend 121) (_ bv103 7)))) (_ bv0 128)) (_ bv1 1) (_ bv0 1)))) (let ((?v_234 (bvor ?v_236 (bvnot ?v_233)))) (let ((?v_307 (ite (= (_ bv1 1) ?v_233) (ite (= (_ bv1 1) ?v_234) ?v_306 (bvadd ?v_306 (_ bv1 128))) ?v_306)) (?v_231 (ite (= (bvand x (bvshl (_ bv1 128) ((_ zero_extend 121) (_ bv102 7)))) (_ bv0 128)) (_ bv1 1) (_ bv0 1)))) (let ((?v_232 (bvor ?v_234 (bvnot ?v_231)))) (let ((?v_308 (ite (= (_ bv1 1) ?v_231) (ite (= (_ bv1 1) ?v_232) ?v_307 (bvadd ?v_307 (_ bv1 128))) ?v_307)) (?v_229 (ite (= (bvand x (bvshl (_ bv1 128) ((_ zero_extend 121) (_ bv101 7)))) (_ bv0 128)) (_ bv1 1) (_ bv0 1)))) (let ((?v_230 (bvor ?v_232 (bvnot ?v_229)))) (let ((?v_309 (ite (= (_ bv1 1) ?v_229) (ite (= (_ bv1 1) ?v_230) ?v_308 (bvadd ?v_308 (_ bv1 128))) ?v_308)) (?v_227 (ite (= (bvand x (bvshl (_ bv1 128) ((_ zero_extend 121) (_ bv100 7)))) (_ bv0 128)) (_ bv1 1) (_ bv0 1)))) (let ((?v_228 (bvor ?v_230 (bvnot ?v_227)))) (let ((?v_310 (ite (= (_ bv1 1) ?v_227) (ite (= (_ bv1 1) ?v_228) ?v_309 (bvadd ?v_309 (_ bv1 128))) ?v_309)) (?v_225 (ite (= (bvand x (bvshl (_ bv1 128) ((_ zero_extend 121) (_ bv99 7)))) (_ bv0 128)) (_ bv1 1) (_ bv0 1)))) (let ((?v_226 (bvor ?v_228 (bvnot ?v_225)))) (let ((?v_311 (ite (= (_ bv1 1) ?v_225) (ite (= (_ bv1 1) ?v_226) ?v_310 (bvadd ?v_310 (_ bv1 128))) ?v_310)) (?v_223 (ite (= (bvand x (bvshl (_ bv1 128) ((_ zero_extend 121) (_ bv98 7)))) (_ bv0 128)) (_ bv1 1) (_ bv0 1)))) (let ((?v_224 (bvor ?v_226 (bvnot ?v_223)))) (let ((?v_312 (ite (= (_ bv1 1) ?v_223) (ite (= (_ bv1 1) ?v_224) ?v_311 (bvadd ?v_311 (_ bv1 128))) ?v_311)) (?v_221 (ite (= (bvand x (bvshl (_ bv1 128) ((_ zero_extend 121) (_ bv97 7)))) (_ bv0 128)) (_ bv1 1) (_ bv0 1)))) (let ((?v_222 (bvor ?v_224 (bvnot ?v_221)))) (let ((?v_313 (ite (= (_ bv1 1) ?v_221) (ite (= (_ bv1 1) ?v_222) ?v_312 (bvadd ?v_312 (_ bv1 128))) ?v_312)) (?v_219 (ite (= (bvand x (bvshl (_ bv1 128) ?v_22)) (_ bv0 128)) (_ bv1 1) (_ bv0 1)))) (let ((?v_220 (bvor ?v_222 (bvnot ?v_219)))) (let ((?v_314 (ite (= (_ bv1 1) ?v_219) (ite (= (_ bv1 1) ?v_220) ?v_313 (bvadd ?v_313 (_ bv1 128))) ?v_313)) (?v_217 (ite (= (bvand x (bvshl (_ bv1 128) ((_ zero_extend 121) (_ bv95 7)))) (_ bv0 128)) (_ bv1 1) (_ bv0 1)))) (let ((?v_218 (bvor ?v_220 (bvnot ?v_217)))) (let ((?v_315 (ite (= (_ bv1 1) ?v_217) (ite (= (_ bv1 1) ?v_218) ?v_314 (bvadd ?v_314 (_ bv1 128))) ?v_314)) (?v_215 (ite (= (bvand x (bvshl (_ bv1 128) ((_ zero_extend 121) (_ bv94 7)))) (_ bv0 128)) (_ bv1 1) (_ bv0 1)))) (let ((?v_216 (bvor ?v_218 (bvnot ?v_215)))) (let ((?v_316 (ite (= (_ bv1 1) ?v_215) (ite (= (_ bv1 1) ?v_216) ?v_315 (bvadd ?v_315 (_ bv1 128))) ?v_315)) (?v_213 (ite (= (bvand x (bvshl (_ bv1 128) ((_ zero_extend 121) (_ bv93 7)))) (_ bv0 128)) (_ bv1 1) (_ bv0 1)))) (let ((?v_214 (bvor ?v_216 (bvnot ?v_213)))) (let ((?v_317 (ite (= (_ bv1 1) ?v_213) (ite (= (_ bv1 1) ?v_214) ?v_316 (bvadd ?v_316 (_ bv1 128))) ?v_316)) (?v_211 (ite (= (bvand x (bvshl (_ bv1 128) ((_ zero_extend 121) (_ bv92 7)))) (_ bv0 128)) (_ bv1 1) (_ bv0 1)))) (let ((?v_212 (bvor ?v_214 (bvnot ?v_211)))) (let ((?v_318 (ite (= (_ bv1 1) ?v_211) (ite (= (_ bv1 1) ?v_212) ?v_317 (bvadd ?v_317 (_ bv1 128))) ?v_317)) (?v_209 (ite (= (bvand x (bvshl (_ bv1 128) ((_ zero_extend 121) (_ bv91 7)))) (_ bv0 128)) (_ bv1 1) (_ bv0 1)))) (let ((?v_210 (bvor ?v_212 (bvnot ?v_209)))) (let ((?v_319 (ite (= (_ bv1 1) ?v_209) (ite (= (_ bv1 1) ?v_210) ?v_318 (bvadd ?v_318 (_ bv1 128))) ?v_318)) (?v_207 (ite (= (bvand x (bvshl (_ bv1 128) ((_ zero_extend 121) (_ bv90 7)))) (_ bv0 128)) (_ bv1 1) (_ bv0 1)))) (let ((?v_208 (bvor ?v_210 (bvnot ?v_207)))) (let ((?v_320 (ite (= (_ bv1 1) ?v_207) (ite (= (_ bv1 1) ?v_208) ?v_319 (bvadd ?v_319 (_ bv1 128))) ?v_319)) (?v_205 (ite (= (bvand x (bvshl (_ bv1 128) ((_ zero_extend 121) (_ bv89 7)))) (_ bv0 128)) (_ bv1 1) (_ bv0 1)))) (let ((?v_206 (bvor ?v_208 (bvnot ?v_205)))) (let ((?v_321 (ite (= (_ bv1 1) ?v_205) (ite (= (_ bv1 1) ?v_206) ?v_320 (bvadd ?v_320 (_ bv1 128))) ?v_320)) (?v_203 (ite (= (bvand x (bvshl (_ bv1 128) ((_ zero_extend 121) (_ bv88 7)))) (_ bv0 128)) (_ bv1 1) (_ bv0 1)))) (let ((?v_204 (bvor ?v_206 (bvnot ?v_203)))) (let ((?v_322 (ite (= (_ bv1 1) ?v_203) (ite (= (_ bv1 1) ?v_204) ?v_321 (bvadd ?v_321 (_ bv1 128))) ?v_321)) (?v_201 (ite (= (bvand x (bvshl (_ bv1 128) ((_ zero_extend 121) (_ bv87 7)))) (_ bv0 128)) (_ bv1 1) (_ bv0 1)))) (let ((?v_202 (bvor ?v_204 (bvnot ?v_201)))) (let ((?v_323 (ite (= (_ bv1 1) ?v_201) (ite (= (_ bv1 1) ?v_202) ?v_322 (bvadd ?v_322 (_ bv1 128))) ?v_322)) (?v_199 (ite (= (bvand x (bvshl (_ bv1 128) ((_ zero_extend 121) (_ bv86 7)))) (_ bv0 128)) (_ bv1 1) (_ bv0 1)))) (let ((?v_200 (bvor ?v_202 (bvnot ?v_199)))) (let ((?v_324 (ite (= (_ bv1 1) ?v_199) (ite (= (_ bv1 1) ?v_200) ?v_323 (bvadd ?v_323 (_ bv1 128))) ?v_323)) (?v_197 (ite (= (bvand x (bvshl (_ bv1 128) ((_ zero_extend 121) (_ bv85 7)))) (_ bv0 128)) (_ bv1 1) (_ bv0 1)))) (let ((?v_198 (bvor ?v_200 (bvnot ?v_197)))) (let ((?v_325 (ite (= (_ bv1 1) ?v_197) (ite (= (_ bv1 1) ?v_198) ?v_324 (bvadd ?v_324 (_ bv1 128))) ?v_324)) (?v_195 (ite (= (bvand x (bvshl (_ bv1 128) ((_ zero_extend 121) (_ bv84 7)))) (_ bv0 128)) (_ bv1 1) (_ bv0 1)))) (let ((?v_196 (bvor ?v_198 (bvnot ?v_195)))) (let ((?v_326 (ite (= (_ bv1 1) ?v_195) (ite (= (_ bv1 1) ?v_196) ?v_325 (bvadd ?v_325 (_ bv1 128))) ?v_325)) (?v_193 (ite (= (bvand x (bvshl (_ bv1 128) ((_ zero_extend 121) (_ bv83 7)))) (_ bv0 128)) (_ bv1 1) (_ bv0 1)))) (let ((?v_194 (bvor ?v_196 (bvnot ?v_193)))) (let ((?v_327 (ite (= (_ bv1 1) ?v_193) (ite (= (_ bv1 1) ?v_194) ?v_326 (bvadd ?v_326 (_ bv1 128))) ?v_326)) (?v_191 (ite (= (bvand x (bvshl (_ bv1 128) ((_ zero_extend 121) (_ bv82 7)))) (_ bv0 128)) (_ bv1 1) (_ bv0 1)))) (let ((?v_192 (bvor ?v_194 (bvnot ?v_191)))) (let ((?v_328 (ite (= (_ bv1 1) ?v_191) (ite (= (_ bv1 1) ?v_192) ?v_327 (bvadd ?v_327 (_ bv1 128))) ?v_327)) (?v_189 (ite (= (bvand x (bvshl (_ bv1 128) ((_ zero_extend 121) (_ bv81 7)))) (_ bv0 128)) (_ bv1 1) (_ bv0 1)))) (let ((?v_190 (bvor ?v_192 (bvnot ?v_189)))) (let ((?v_329 (ite (= (_ bv1 1) ?v_189) (ite (= (_ bv1 1) ?v_190) ?v_328 (bvadd ?v_328 (_ bv1 128))) ?v_328)) (?v_187 (ite (= (bvand x (bvshl (_ bv1 128) ((_ zero_extend 121) (_ bv80 7)))) (_ bv0 128)) (_ bv1 1) (_ bv0 1)))) (let ((?v_188 (bvor ?v_190 (bvnot ?v_187)))) (let ((?v_330 (ite (= (_ bv1 1) ?v_187) (ite (= (_ bv1 1) ?v_188) ?v_329 (bvadd ?v_329 (_ bv1 128))) ?v_329)) (?v_185 (ite (= (bvand x (bvshl (_ bv1 128) ((_ zero_extend 121) (_ bv79 7)))) (_ bv0 128)) (_ bv1 1) (_ bv0 1)))) (let ((?v_186 (bvor ?v_188 (bvnot ?v_185)))) (let ((?v_331 (ite (= (_ bv1 1) ?v_185) (ite (= (_ bv1 1) ?v_186) ?v_330 (bvadd ?v_330 (_ bv1 128))) ?v_330)) (?v_183 (ite (= (bvand x (bvshl (_ bv1 128) ((_ zero_extend 121) (_ bv78 7)))) (_ bv0 128)) (_ bv1 1) (_ bv0 1)))) (let ((?v_184 (bvor ?v_186 (bvnot ?v_183)))) (let ((?v_332 (ite (= (_ bv1 1) ?v_183) (ite (= (_ bv1 1) ?v_184) ?v_331 (bvadd ?v_331 (_ bv1 128))) ?v_331)) (?v_181 (ite (= (bvand x (bvshl (_ bv1 128) ((_ zero_extend 121) (_ bv77 7)))) (_ bv0 128)) (_ bv1 1) (_ bv0 1)))) (let ((?v_182 (bvor ?v_184 (bvnot ?v_181)))) (let ((?v_333 (ite (= (_ bv1 1) ?v_181) (ite (= (_ bv1 1) ?v_182) ?v_332 (bvadd ?v_332 (_ bv1 128))) ?v_332)) (?v_179 (ite (= (bvand x (bvshl (_ bv1 128) ((_ zero_extend 121) (_ bv76 7)))) (_ bv0 128)) (_ bv1 1) (_ bv0 1)))) (let ((?v_180 (bvor ?v_182 (bvnot ?v_179)))) (let ((?v_334 (ite (= (_ bv1 1) ?v_179) (ite (= (_ bv1 1) ?v_180) ?v_333 (bvadd ?v_333 (_ bv1 128))) ?v_333)) (?v_177 (ite (= (bvand x (bvshl (_ bv1 128) ((_ zero_extend 121) (_ bv75 7)))) (_ bv0 128)) (_ bv1 1) (_ bv0 1)))) (let ((?v_178 (bvor ?v_180 (bvnot ?v_177)))) (let ((?v_335 (ite (= (_ bv1 1) ?v_177) (ite (= (_ bv1 1) ?v_178) ?v_334 (bvadd ?v_334 (_ bv1 128))) ?v_334)) (?v_175 (ite (= (bvand x (bvshl (_ bv1 128) ((_ zero_extend 121) (_ bv74 7)))) (_ bv0 128)) (_ bv1 1) (_ bv0 1)))) (let ((?v_176 (bvor ?v_178 (bvnot ?v_175)))) (let ((?v_336 (ite (= (_ bv1 1) ?v_175) (ite (= (_ bv1 1) ?v_176) ?v_335 (bvadd ?v_335 (_ bv1 128))) ?v_335)) (?v_173 (ite (= (bvand x (bvshl (_ bv1 128) ((_ zero_extend 121) (_ bv73 7)))) (_ bv0 128)) (_ bv1 1) (_ bv0 1)))) (let ((?v_174 (bvor ?v_176 (bvnot ?v_173)))) (let ((?v_337 (ite (= (_ bv1 1) ?v_173) (ite (= (_ bv1 1) ?v_174) ?v_336 (bvadd ?v_336 (_ bv1 128))) ?v_336)) (?v_171 (ite (= (bvand x (bvshl (_ bv1 128) ((_ zero_extend 121) (_ bv72 7)))) (_ bv0 128)) (_ bv1 1) (_ bv0 1)))) (let ((?v_172 (bvor ?v_174 (bvnot ?v_171)))) (let ((?v_338 (ite (= (_ bv1 1) ?v_171) (ite (= (_ bv1 1) ?v_172) ?v_337 (bvadd ?v_337 (_ bv1 128))) ?v_337)) (?v_169 (ite (= (bvand x (bvshl (_ bv1 128) ((_ zero_extend 121) (_ bv71 7)))) (_ bv0 128)) (_ bv1 1) (_ bv0 1)))) (let ((?v_170 (bvor ?v_172 (bvnot ?v_169)))) (let ((?v_339 (ite (= (_ bv1 1) ?v_169) (ite (= (_ bv1 1) ?v_170) ?v_338 (bvadd ?v_338 (_ bv1 128))) ?v_338)) (?v_167 (ite (= (bvand x (bvshl (_ bv1 128) ((_ zero_extend 121) (_ bv70 7)))) (_ bv0 128)) (_ bv1 1) (_ bv0 1)))) (let ((?v_168 (bvor ?v_170 (bvnot ?v_167)))) (let ((?v_340 (ite (= (_ bv1 1) ?v_167) (ite (= (_ bv1 1) ?v_168) ?v_339 (bvadd ?v_339 (_ bv1 128))) ?v_339)) (?v_165 (ite (= (bvand x (bvshl (_ bv1 128) ((_ zero_extend 121) (_ bv69 7)))) (_ bv0 128)) (_ bv1 1) (_ bv0 1)))) (let ((?v_166 (bvor ?v_168 (bvnot ?v_165)))) (let ((?v_341 (ite (= (_ bv1 1) ?v_165) (ite (= (_ bv1 1) ?v_166) ?v_340 (bvadd ?v_340 (_ bv1 128))) ?v_340)) (?v_163 (ite (= (bvand x (bvshl (_ bv1 128) ((_ zero_extend 121) (_ bv68 7)))) (_ bv0 128)) (_ bv1 1) (_ bv0 1)))) (let ((?v_164 (bvor ?v_166 (bvnot ?v_163)))) (let ((?v_342 (ite (= (_ bv1 1) ?v_163) (ite (= (_ bv1 1) ?v_164) ?v_341 (bvadd ?v_341 (_ bv1 128))) ?v_341)) (?v_161 (ite (= (bvand x (bvshl (_ bv1 128) ((_ zero_extend 121) (_ bv67 7)))) (_ bv0 128)) (_ bv1 1) (_ bv0 1)))) (let ((?v_162 (bvor ?v_164 (bvnot ?v_161)))) (let ((?v_343 (ite (= (_ bv1 1) ?v_161) (ite (= (_ bv1 1) ?v_162) ?v_342 (bvadd ?v_342 (_ bv1 128))) ?v_342)) (?v_159 (ite (= (bvand x (bvshl (_ bv1 128) ((_ zero_extend 121) (_ bv66 7)))) (_ bv0 128)) (_ bv1 1) (_ bv0 1)))) (let ((?v_160 (bvor ?v_162 (bvnot ?v_159)))) (let ((?v_344 (ite (= (_ bv1 1) ?v_159) (ite (= (_ bv1 1) ?v_160) ?v_343 (bvadd ?v_343 (_ bv1 128))) ?v_343)) (?v_157 (ite (= (bvand x (bvshl (_ bv1 128) ((_ zero_extend 121) (_ bv65 7)))) (_ bv0 128)) (_ bv1 1) (_ bv0 1)))) (let ((?v_158 (bvor ?v_160 (bvnot ?v_157)))) (let ((?v_345 (ite (= (_ bv1 1) ?v_157) (ite (= (_ bv1 1) ?v_158) ?v_344 (bvadd ?v_344 (_ bv1 128))) ?v_344)) (?v_155 (ite (= (bvand x (bvshl (_ bv1 128) ?v_0)) (_ bv0 128)) (_ bv1 1) (_ bv0 1)))) (let ((?v_156 (bvor ?v_158 (bvnot ?v_155)))) (let ((?v_346 (ite (= (_ bv1 1) ?v_155) (ite (= (_ bv1 1) ?v_156) ?v_345 (bvadd ?v_345 (_ bv1 128))) ?v_345)) (?v_153 (ite (= (bvand x (bvshl (_ bv1 128) ((_ zero_extend 121) (_ bv63 7)))) (_ bv0 128)) (_ bv1 1) (_ bv0 1)))) (let ((?v_154 (bvor ?v_156 (bvnot ?v_153)))) (let ((?v_347 (ite (= (_ bv1 1) ?v_153) (ite (= (_ bv1 1) ?v_154) ?v_346 (bvadd ?v_346 (_ bv1 128))) ?v_346)) (?v_151 (ite (= (bvand x (bvshl (_ bv1 128) ((_ zero_extend 121) (_ bv62 7)))) (_ bv0 128)) (_ bv1 1) (_ bv0 1)))) (let ((?v_152 (bvor ?v_154 (bvnot ?v_151)))) (let ((?v_348 (ite (= (_ bv1 1) ?v_151) (ite (= (_ bv1 1) ?v_152) ?v_347 (bvadd ?v_347 (_ bv1 128))) ?v_347)) (?v_149 (ite (= (bvand x (bvshl (_ bv1 128) ((_ zero_extend 121) (_ bv61 7)))) (_ bv0 128)) (_ bv1 1) (_ bv0 1)))) (let ((?v_150 (bvor ?v_152 (bvnot ?v_149)))) (let ((?v_349 (ite (= (_ bv1 1) ?v_149) (ite (= (_ bv1 1) ?v_150) ?v_348 (bvadd ?v_348 (_ bv1 128))) ?v_348)) (?v_147 (ite (= (bvand x (bvshl (_ bv1 128) ((_ zero_extend 121) (_ bv60 7)))) (_ bv0 128)) (_ bv1 1) (_ bv0 1)))) (let ((?v_148 (bvor ?v_150 (bvnot ?v_147)))) (let ((?v_350 (ite (= (_ bv1 1) ?v_147) (ite (= (_ bv1 1) ?v_148) ?v_349 (bvadd ?v_349 (_ bv1 128))) ?v_349)) (?v_145 (ite (= (bvand x (bvshl (_ bv1 128) ((_ zero_extend 121) (_ bv59 7)))) (_ bv0 128)) (_ bv1 1) (_ bv0 1)))) (let ((?v_146 (bvor ?v_148 (bvnot ?v_145)))) (let ((?v_351 (ite (= (_ bv1 1) ?v_145) (ite (= (_ bv1 1) ?v_146) ?v_350 (bvadd ?v_350 (_ bv1 128))) ?v_350)) (?v_143 (ite (= (bvand x (bvshl (_ bv1 128) ((_ zero_extend 121) (_ bv58 7)))) (_ bv0 128)) (_ bv1 1) (_ bv0 1)))) (let ((?v_144 (bvor ?v_146 (bvnot ?v_143)))) (let ((?v_352 (ite (= (_ bv1 1) ?v_143) (ite (= (_ bv1 1) ?v_144) ?v_351 (bvadd ?v_351 (_ bv1 128))) ?v_351)) (?v_141 (ite (= (bvand x (bvshl (_ bv1 128) ((_ zero_extend 121) (_ bv57 7)))) (_ bv0 128)) (_ bv1 1) (_ bv0 1)))) (let ((?v_142 (bvor ?v_144 (bvnot ?v_141)))) (let ((?v_353 (ite (= (_ bv1 1) ?v_141) (ite (= (_ bv1 1) ?v_142) ?v_352 (bvadd ?v_352 (_ bv1 128))) ?v_352)) (?v_139 (ite (= (bvand x (bvshl (_ bv1 128) ((_ zero_extend 121) (_ bv56 7)))) (_ bv0 128)) (_ bv1 1) (_ bv0 1)))) (let ((?v_140 (bvor ?v_142 (bvnot ?v_139)))) (let ((?v_354 (ite (= (_ bv1 1) ?v_139) (ite (= (_ bv1 1) ?v_140) ?v_353 (bvadd ?v_353 (_ bv1 128))) ?v_353)) (?v_137 (ite (= (bvand x (bvshl (_ bv1 128) ((_ zero_extend 121) (_ bv55 7)))) (_ bv0 128)) (_ bv1 1) (_ bv0 1)))) (let ((?v_138 (bvor ?v_140 (bvnot ?v_137)))) (let ((?v_355 (ite (= (_ bv1 1) ?v_137) (ite (= (_ bv1 1) ?v_138) ?v_354 (bvadd ?v_354 (_ bv1 128))) ?v_354)) (?v_135 (ite (= (bvand x (bvshl (_ bv1 128) ((_ zero_extend 121) (_ bv54 7)))) (_ bv0 128)) (_ bv1 1) (_ bv0 1)))) (let ((?v_136 (bvor ?v_138 (bvnot ?v_135)))) (let ((?v_356 (ite (= (_ bv1 1) ?v_135) (ite (= (_ bv1 1) ?v_136) ?v_355 (bvadd ?v_355 (_ bv1 128))) ?v_355)) (?v_133 (ite (= (bvand x (bvshl (_ bv1 128) ((_ zero_extend 121) (_ bv53 7)))) (_ bv0 128)) (_ bv1 1) (_ bv0 1)))) (let ((?v_134 (bvor ?v_136 (bvnot ?v_133)))) (let ((?v_357 (ite (= (_ bv1 1) ?v_133) (ite (= (_ bv1 1) ?v_134) ?v_356 (bvadd ?v_356 (_ bv1 128))) ?v_356)) (?v_131 (ite (= (bvand x (bvshl (_ bv1 128) ((_ zero_extend 121) (_ bv52 7)))) (_ bv0 128)) (_ bv1 1) (_ bv0 1)))) (let ((?v_132 (bvor ?v_134 (bvnot ?v_131)))) (let ((?v_358 (ite (= (_ bv1 1) ?v_131) (ite (= (_ bv1 1) ?v_132) ?v_357 (bvadd ?v_357 (_ bv1 128))) ?v_357)) (?v_129 (ite (= (bvand x (bvshl (_ bv1 128) ((_ zero_extend 121) (_ bv51 7)))) (_ bv0 128)) (_ bv1 1) (_ bv0 1)))) (let ((?v_130 (bvor ?v_132 (bvnot ?v_129)))) (let ((?v_359 (ite (= (_ bv1 1) ?v_129) (ite (= (_ bv1 1) ?v_130) ?v_358 (bvadd ?v_358 (_ bv1 128))) ?v_358)) (?v_127 (ite (= (bvand x (bvshl (_ bv1 128) ((_ zero_extend 121) (_ bv50 7)))) (_ bv0 128)) (_ bv1 1) (_ bv0 1)))) (let ((?v_128 (bvor ?v_130 (bvnot ?v_127)))) (let ((?v_360 (ite (= (_ bv1 1) ?v_127) (ite (= (_ bv1 1) ?v_128) ?v_359 (bvadd ?v_359 (_ bv1 128))) ?v_359)) (?v_125 (ite (= (bvand x (bvshl (_ bv1 128) ((_ zero_extend 121) (_ bv49 7)))) (_ bv0 128)) (_ bv1 1) (_ bv0 1)))) (let ((?v_126 (bvor ?v_128 (bvnot ?v_125)))) (let ((?v_361 (ite (= (_ bv1 1) ?v_125) (ite (= (_ bv1 1) ?v_126) ?v_360 (bvadd ?v_360 (_ bv1 128))) ?v_360)) (?v_123 (ite (= (bvand x (bvshl (_ bv1 128) ((_ zero_extend 121) (_ bv48 7)))) (_ bv0 128)) (_ bv1 1) (_ bv0 1)))) (let ((?v_124 (bvor ?v_126 (bvnot ?v_123)))) (let ((?v_362 (ite (= (_ bv1 1) ?v_123) (ite (= (_ bv1 1) ?v_124) ?v_361 (bvadd ?v_361 (_ bv1 128))) ?v_361)) (?v_121 (ite (= (bvand x (bvshl (_ bv1 128) ((_ zero_extend 121) (_ bv47 7)))) (_ bv0 128)) (_ bv1 1) (_ bv0 1)))) (let ((?v_122 (bvor ?v_124 (bvnot ?v_121)))) (let ((?v_363 (ite (= (_ bv1 1) ?v_121) (ite (= (_ bv1 1) ?v_122) ?v_362 (bvadd ?v_362 (_ bv1 128))) ?v_362)) (?v_119 (ite (= (bvand x (bvshl (_ bv1 128) ((_ zero_extend 121) (_ bv46 7)))) (_ bv0 128)) (_ bv1 1) (_ bv0 1)))) (let ((?v_120 (bvor ?v_122 (bvnot ?v_119)))) (let ((?v_364 (ite (= (_ bv1 1) ?v_119) (ite (= (_ bv1 1) ?v_120) ?v_363 (bvadd ?v_363 (_ bv1 128))) ?v_363)) (?v_117 (ite (= (bvand x (bvshl (_ bv1 128) ((_ zero_extend 121) (_ bv45 7)))) (_ bv0 128)) (_ bv1 1) (_ bv0 1)))) (let ((?v_118 (bvor ?v_120 (bvnot ?v_117)))) (let ((?v_365 (ite (= (_ bv1 1) ?v_117) (ite (= (_ bv1 1) ?v_118) ?v_364 (bvadd ?v_364 (_ bv1 128))) ?v_364)) (?v_115 (ite (= (bvand x (bvshl (_ bv1 128) ((_ zero_extend 121) (_ bv44 7)))) (_ bv0 128)) (_ bv1 1) (_ bv0 1)))) (let ((?v_116 (bvor ?v_118 (bvnot ?v_115)))) (let ((?v_366 (ite (= (_ bv1 1) ?v_115) (ite (= (_ bv1 1) ?v_116) ?v_365 (bvadd ?v_365 (_ bv1 128))) ?v_365)) (?v_113 (ite (= (bvand x (bvshl (_ bv1 128) ((_ zero_extend 121) (_ bv43 7)))) (_ bv0 128)) (_ bv1 1) (_ bv0 1)))) (let ((?v_114 (bvor ?v_116 (bvnot ?v_113)))) (let ((?v_367 (ite (= (_ bv1 1) ?v_113) (ite (= (_ bv1 1) ?v_114) ?v_366 (bvadd ?v_366 (_ bv1 128))) ?v_366)) (?v_111 (ite (= (bvand x (bvshl (_ bv1 128) ((_ zero_extend 121) (_ bv42 7)))) (_ bv0 128)) (_ bv1 1) (_ bv0 1)))) (let ((?v_112 (bvor ?v_114 (bvnot ?v_111)))) (let ((?v_368 (ite (= (_ bv1 1) ?v_111) (ite (= (_ bv1 1) ?v_112) ?v_367 (bvadd ?v_367 (_ bv1 128))) ?v_367)) (?v_109 (ite (= (bvand x (bvshl (_ bv1 128) ((_ zero_extend 121) (_ bv41 7)))) (_ bv0 128)) (_ bv1 1) (_ bv0 1)))) (let ((?v_110 (bvor ?v_112 (bvnot ?v_109)))) (let ((?v_369 (ite (= (_ bv1 1) ?v_109) (ite (= (_ bv1 1) ?v_110) ?v_368 (bvadd ?v_368 (_ bv1 128))) ?v_368)) (?v_107 (ite (= (bvand x (bvshl (_ bv1 128) ((_ zero_extend 121) (_ bv40 7)))) (_ bv0 128)) (_ bv1 1) (_ bv0 1)))) (let ((?v_108 (bvor ?v_110 (bvnot ?v_107)))) (let ((?v_370 (ite (= (_ bv1 1) ?v_107) (ite (= (_ bv1 1) ?v_108) ?v_369 (bvadd ?v_369 (_ bv1 128))) ?v_369)) (?v_105 (ite (= (bvand x (bvshl (_ bv1 128) ((_ zero_extend 121) (_ bv39 7)))) (_ bv0 128)) (_ bv1 1) (_ bv0 1)))) (let ((?v_106 (bvor ?v_108 (bvnot ?v_105)))) (let ((?v_371 (ite (= (_ bv1 1) ?v_105) (ite (= (_ bv1 1) ?v_106) ?v_370 (bvadd ?v_370 (_ bv1 128))) ?v_370)) (?v_103 (ite (= (bvand x (bvshl (_ bv1 128) ((_ zero_extend 121) (_ bv38 7)))) (_ bv0 128)) (_ bv1 1) (_ bv0 1)))) (let ((?v_104 (bvor ?v_106 (bvnot ?v_103)))) (let ((?v_372 (ite (= (_ bv1 1) ?v_103) (ite (= (_ bv1 1) ?v_104) ?v_371 (bvadd ?v_371 (_ bv1 128))) ?v_371)) (?v_101 (ite (= (bvand x (bvshl (_ bv1 128) ((_ zero_extend 121) (_ bv37 7)))) (_ bv0 128)) (_ bv1 1) (_ bv0 1)))) (let ((?v_102 (bvor ?v_104 (bvnot ?v_101)))) (let ((?v_373 (ite (= (_ bv1 1) ?v_101) (ite (= (_ bv1 1) ?v_102) ?v_372 (bvadd ?v_372 (_ bv1 128))) ?v_372)) (?v_99 (ite (= (bvand x (bvshl (_ bv1 128) ((_ zero_extend 121) (_ bv36 7)))) (_ bv0 128)) (_ bv1 1) (_ bv0 1)))) (let ((?v_100 (bvor ?v_102 (bvnot ?v_99)))) (let ((?v_374 (ite (= (_ bv1 1) ?v_99) (ite (= (_ bv1 1) ?v_100) ?v_373 (bvadd ?v_373 (_ bv1 128))) ?v_373)) (?v_97 (ite (= (bvand x (bvshl (_ bv1 128) ((_ zero_extend 121) (_ bv35 7)))) (_ bv0 128)) (_ bv1 1) (_ bv0 1)))) (let ((?v_98 (bvor ?v_100 (bvnot ?v_97)))) (let ((?v_375 (ite (= (_ bv1 1) ?v_97) (ite (= (_ bv1 1) ?v_98) ?v_374 (bvadd ?v_374 (_ bv1 128))) ?v_374)) (?v_95 (ite (= (bvand x (bvshl (_ bv1 128) ((_ zero_extend 121) (_ bv34 7)))) (_ bv0 128)) (_ bv1 1) (_ bv0 1)))) (let ((?v_96 (bvor ?v_98 (bvnot ?v_95)))) (let ((?v_376 (ite (= (_ bv1 1) ?v_95) (ite (= (_ bv1 1) ?v_96) ?v_375 (bvadd ?v_375 (_ bv1 128))) ?v_375)) (?v_93 (ite (= (bvand x (bvshl (_ bv1 128) ((_ zero_extend 121) (_ bv33 7)))) (_ bv0 128)) (_ bv1 1) (_ bv0 1)))) (let ((?v_94 (bvor ?v_96 (bvnot ?v_93)))) (let ((?v_377 (ite (= (_ bv1 1) ?v_93) (ite (= (_ bv1 1) ?v_94) ?v_376 (bvadd ?v_376 (_ bv1 128))) ?v_376)) (?v_91 (ite (= (bvand x (bvshl (_ bv1 128) ?v_23)) (_ bv0 128)) (_ bv1 1) (_ bv0 1)))) (let ((?v_92 (bvor ?v_94 (bvnot ?v_91)))) (let ((?v_378 (ite (= (_ bv1 1) ?v_91) (ite (= (_ bv1 1) ?v_92) ?v_377 (bvadd ?v_377 (_ bv1 128))) ?v_377)) (?v_89 (ite (= (bvand x (bvshl (_ bv1 128) ((_ zero_extend 121) (_ bv31 7)))) (_ bv0 128)) (_ bv1 1) (_ bv0 1)))) (let ((?v_90 (bvor ?v_92 (bvnot ?v_89)))) (let ((?v_379 (ite (= (_ bv1 1) ?v_89) (ite (= (_ bv1 1) ?v_90) ?v_378 (bvadd ?v_378 (_ bv1 128))) ?v_378)) (?v_87 (ite (= (bvand x (bvshl (_ bv1 128) ((_ zero_extend 121) (_ bv30 7)))) (_ bv0 128)) (_ bv1 1) (_ bv0 1)))) (let ((?v_88 (bvor ?v_90 (bvnot ?v_87)))) (let ((?v_380 (ite (= (_ bv1 1) ?v_87) (ite (= (_ bv1 1) ?v_88) ?v_379 (bvadd ?v_379 (_ bv1 128))) ?v_379)) (?v_85 (ite (= (bvand x (bvshl (_ bv1 128) ((_ zero_extend 121) (_ bv29 7)))) (_ bv0 128)) (_ bv1 1) (_ bv0 1)))) (let ((?v_86 (bvor ?v_88 (bvnot ?v_85)))) (let ((?v_381 (ite (= (_ bv1 1) ?v_85) (ite (= (_ bv1 1) ?v_86) ?v_380 (bvadd ?v_380 (_ bv1 128))) ?v_380)) (?v_83 (ite (= (bvand x (bvshl (_ bv1 128) ((_ zero_extend 121) (_ bv28 7)))) (_ bv0 128)) (_ bv1 1) (_ bv0 1)))) (let ((?v_84 (bvor ?v_86 (bvnot ?v_83)))) (let ((?v_382 (ite (= (_ bv1 1) ?v_83) (ite (= (_ bv1 1) ?v_84) ?v_381 (bvadd ?v_381 (_ bv1 128))) ?v_381)) (?v_81 (ite (= (bvand x (bvshl (_ bv1 128) ((_ zero_extend 121) (_ bv27 7)))) (_ bv0 128)) (_ bv1 1) (_ bv0 1)))) (let ((?v_82 (bvor ?v_84 (bvnot ?v_81)))) (let ((?v_383 (ite (= (_ bv1 1) ?v_81) (ite (= (_ bv1 1) ?v_82) ?v_382 (bvadd ?v_382 (_ bv1 128))) ?v_382)) (?v_79 (ite (= (bvand x (bvshl (_ bv1 128) ((_ zero_extend 121) (_ bv26 7)))) (_ bv0 128)) (_ bv1 1) (_ bv0 1)))) (let ((?v_80 (bvor ?v_82 (bvnot ?v_79)))) (let ((?v_384 (ite (= (_ bv1 1) ?v_79) (ite (= (_ bv1 1) ?v_80) ?v_383 (bvadd ?v_383 (_ bv1 128))) ?v_383)) (?v_77 (ite (= (bvand x (bvshl (_ bv1 128) ((_ zero_extend 121) (_ bv25 7)))) (_ bv0 128)) (_ bv1 1) (_ bv0 1)))) (let ((?v_78 (bvor ?v_80 (bvnot ?v_77)))) (let ((?v_385 (ite (= (_ bv1 1) ?v_77) (ite (= (_ bv1 1) ?v_78) ?v_384 (bvadd ?v_384 (_ bv1 128))) ?v_384)) (?v_75 (ite (= (bvand x (bvshl (_ bv1 128) ((_ zero_extend 121) (_ bv24 7)))) (_ bv0 128)) (_ bv1 1) (_ bv0 1)))) (let ((?v_76 (bvor ?v_78 (bvnot ?v_75)))) (let ((?v_386 (ite (= (_ bv1 1) ?v_75) (ite (= (_ bv1 1) ?v_76) ?v_385 (bvadd ?v_385 (_ bv1 128))) ?v_385)) (?v_73 (ite (= (bvand x (bvshl (_ bv1 128) ((_ zero_extend 121) (_ bv23 7)))) (_ bv0 128)) (_ bv1 1) (_ bv0 1)))) (let ((?v_74 (bvor ?v_76 (bvnot ?v_73)))) (let ((?v_387 (ite (= (_ bv1 1) ?v_73) (ite (= (_ bv1 1) ?v_74) ?v_386 (bvadd ?v_386 (_ bv1 128))) ?v_386)) (?v_71 (ite (= (bvand x (bvshl (_ bv1 128) ((_ zero_extend 121) (_ bv22 7)))) (_ bv0 128)) (_ bv1 1) (_ bv0 1)))) (let ((?v_72 (bvor ?v_74 (bvnot ?v_71)))) (let ((?v_388 (ite (= (_ bv1 1) ?v_71) (ite (= (_ bv1 1) ?v_72) ?v_387 (bvadd ?v_387 (_ bv1 128))) ?v_387)) (?v_69 (ite (= (bvand x (bvshl (_ bv1 128) ((_ zero_extend 121) (_ bv21 7)))) (_ bv0 128)) (_ bv1 1) (_ bv0 1)))) (let ((?v_70 (bvor ?v_72 (bvnot ?v_69)))) (let ((?v_389 (ite (= (_ bv1 1) ?v_69) (ite (= (_ bv1 1) ?v_70) ?v_388 (bvadd ?v_388 (_ bv1 128))) ?v_388)) (?v_67 (ite (= (bvand x (bvshl (_ bv1 128) ((_ zero_extend 121) (_ bv20 7)))) (_ bv0 128)) (_ bv1 1) (_ bv0 1)))) (let ((?v_68 (bvor ?v_70 (bvnot ?v_67)))) (let ((?v_390 (ite (= (_ bv1 1) ?v_67) (ite (= (_ bv1 1) ?v_68) ?v_389 (bvadd ?v_389 (_ bv1 128))) ?v_389)) (?v_65 (ite (= (bvand x (bvshl (_ bv1 128) ((_ zero_extend 121) (_ bv19 7)))) (_ bv0 128)) (_ bv1 1) (_ bv0 1)))) (let ((?v_66 (bvor ?v_68 (bvnot ?v_65)))) (let ((?v_391 (ite (= (_ bv1 1) ?v_65) (ite (= (_ bv1 1) ?v_66) ?v_390 (bvadd ?v_390 (_ bv1 128))) ?v_390)) (?v_63 (ite (= (bvand x (bvshl (_ bv1 128) ((_ zero_extend 121) (_ bv18 7)))) (_ bv0 128)) (_ bv1 1) (_ bv0 1)))) (let ((?v_64 (bvor ?v_66 (bvnot ?v_63)))) (let ((?v_392 (ite (= (_ bv1 1) ?v_63) (ite (= (_ bv1 1) ?v_64) ?v_391 (bvadd ?v_391 (_ bv1 128))) ?v_391)) (?v_61 (ite (= (bvand x (bvshl (_ bv1 128) ((_ zero_extend 121) (_ bv17 7)))) (_ bv0 128)) (_ bv1 1) (_ bv0 1)))) (let ((?v_62 (bvor ?v_64 (bvnot ?v_61)))) (let ((?v_393 (ite (= (_ bv1 1) ?v_61) (ite (= (_ bv1 1) ?v_62) ?v_392 (bvadd ?v_392 (_ bv1 128))) ?v_392)) (?v_59 (ite (= (bvand x (bvshl (_ bv1 128) ?v_24)) (_ bv0 128)) (_ bv1 1) (_ bv0 1)))) (let ((?v_60 (bvor ?v_62 (bvnot ?v_59)))) (let ((?v_394 (ite (= (_ bv1 1) ?v_59) (ite (= (_ bv1 1) ?v_60) ?v_393 (bvadd ?v_393 (_ bv1 128))) ?v_393)) (?v_57 (ite (= (bvand x (bvshl (_ bv1 128) ((_ zero_extend 121) (_ bv15 7)))) (_ bv0 128)) (_ bv1 1) (_ bv0 1)))) (let ((?v_58 (bvor ?v_60 (bvnot ?v_57)))) (let ((?v_395 (ite (= (_ bv1 1) ?v_57) (ite (= (_ bv1 1) ?v_58) ?v_394 (bvadd ?v_394 (_ bv1 128))) ?v_394)) (?v_55 (ite (= (bvand x (bvshl (_ bv1 128) ((_ zero_extend 121) (_ bv14 7)))) (_ bv0 128)) (_ bv1 1) (_ bv0 1)))) (let ((?v_56 (bvor ?v_58 (bvnot ?v_55)))) (let ((?v_396 (ite (= (_ bv1 1) ?v_55) (ite (= (_ bv1 1) ?v_56) ?v_395 (bvadd ?v_395 (_ bv1 128))) ?v_395)) (?v_53 (ite (= (bvand x (bvshl (_ bv1 128) ((_ zero_extend 121) (_ bv13 7)))) (_ bv0 128)) (_ bv1 1) (_ bv0 1)))) (let ((?v_54 (bvor ?v_56 (bvnot ?v_53)))) (let ((?v_397 (ite (= (_ bv1 1) ?v_53) (ite (= (_ bv1 1) ?v_54) ?v_396 (bvadd ?v_396 (_ bv1 128))) ?v_396)) (?v_51 (ite (= (bvand x (bvshl (_ bv1 128) ((_ zero_extend 121) (_ bv12 7)))) (_ bv0 128)) (_ bv1 1) (_ bv0 1)))) (let ((?v_52 (bvor ?v_54 (bvnot ?v_51)))) (let ((?v_398 (ite (= (_ bv1 1) ?v_51) (ite (= (_ bv1 1) ?v_52) ?v_397 (bvadd ?v_397 (_ bv1 128))) ?v_397)) (?v_49 (ite (= (bvand x (bvshl (_ bv1 128) ((_ zero_extend 121) (_ bv11 7)))) (_ bv0 128)) (_ bv1 1) (_ bv0 1)))) (let ((?v_50 (bvor ?v_52 (bvnot ?v_49)))) (let ((?v_399 (ite (= (_ bv1 1) ?v_49) (ite (= (_ bv1 1) ?v_50) ?v_398 (bvadd ?v_398 (_ bv1 128))) ?v_398)) (?v_47 (ite (= (bvand x (bvshl (_ bv1 128) ((_ zero_extend 121) (_ bv10 7)))) (_ bv0 128)) (_ bv1 1) (_ bv0 1)))) (let ((?v_48 (bvor ?v_50 (bvnot ?v_47)))) (let ((?v_400 (ite (= (_ bv1 1) ?v_47) (ite (= (_ bv1 1) ?v_48) ?v_399 (bvadd ?v_399 (_ bv1 128))) ?v_399)) (?v_45 (ite (= (bvand x (bvshl (_ bv1 128) ((_ zero_extend 121) (_ bv9 7)))) (_ bv0 128)) (_ bv1 1) (_ bv0 1)))) (let ((?v_46 (bvor ?v_48 (bvnot ?v_45)))) (let ((?v_401 (ite (= (_ bv1 1) ?v_45) (ite (= (_ bv1 1) ?v_46) ?v_400 (bvadd ?v_400 (_ bv1 128))) ?v_400)) (?v_43 (ite (= (bvand x (bvshl (_ bv1 128) ?v_25)) (_ bv0 128)) (_ bv1 1) (_ bv0 1)))) (let ((?v_44 (bvor ?v_46 (bvnot ?v_43)))) (let ((?v_402 (ite (= (_ bv1 1) ?v_43) (ite (= (_ bv1 1) ?v_44) ?v_401 (bvadd ?v_401 (_ bv1 128))) ?v_401)) (?v_41 (ite (= (bvand x (bvshl (_ bv1 128) ((_ zero_extend 121) (_ bv7 7)))) (_ bv0 128)) (_ bv1 1) (_ bv0 1)))) (let ((?v_42 (bvor ?v_44 (bvnot ?v_41)))) (let ((?v_403 (ite (= (_ bv1 1) ?v_41) (ite (= (_ bv1 1) ?v_42) ?v_402 (bvadd ?v_402 (_ bv1 128))) ?v_402)) (?v_39 (ite (= (bvand x (bvshl (_ bv1 128) ((_ zero_extend 121) (_ bv6 7)))) (_ bv0 128)) (_ bv1 1) (_ bv0 1)))) (let ((?v_40 (bvor ?v_42 (bvnot ?v_39)))) (let ((?v_404 (ite (= (_ bv1 1) ?v_39) (ite (= (_ bv1 1) ?v_40) ?v_403 (bvadd ?v_403 (_ bv1 128))) ?v_403)) (?v_37 (ite (= (bvand x (bvshl (_ bv1 128) ((_ zero_extend 121) (_ bv5 7)))) (_ bv0 128)) (_ bv1 1) (_ bv0 1)))) (let ((?v_38 (bvor ?v_40 (bvnot ?v_37)))) (let ((?v_405 (ite (= (_ bv1 1) ?v_37) (ite (= (_ bv1 1) ?v_38) ?v_404 (bvadd ?v_404 (_ bv1 128))) ?v_404)) (?v_35 (ite (= (bvand x (bvshl (_ bv1 128) ?v_26)) (_ bv0 128)) (_ bv1 1) (_ bv0 1)))) (let ((?v_36 (bvor ?v_38 (bvnot ?v_35)))) (let ((?v_406 (ite (= (_ bv1 1) ?v_35) (ite (= (_ bv1 1) ?v_36) ?v_405 (bvadd ?v_405 (_ bv1 128))) ?v_405)) (?v_33 (ite (= (bvand x (bvshl (_ bv1 128) ((_ zero_extend 121) (_ bv3 7)))) (_ bv0 128)) (_ bv1 1) (_ bv0 1)))) (let ((?v_34 (bvor ?v_36 (bvnot ?v_33)))) (let ((?v_407 (ite (= (_ bv1 1) ?v_33) (ite (= (_ bv1 1) ?v_34) ?v_406 (bvadd ?v_406 (_ bv1 128))) ?v_406)) (?v_31 (ite (= (bvand x (bvshl (_ bv1 128) ?v_27)) (_ bv0 128)) (_ bv1 1) (_ bv0 1)))) (let ((?v_32 (bvor ?v_34 (bvnot ?v_31)))) (let ((?v_408 (ite (= (_ bv1 1) ?v_31) (ite (= (_ bv1 1) ?v_32) ?v_407 (bvadd ?v_407 (_ bv1 128))) ?v_407)) (?v_29 (ite (= (bvand x (bvshl (_ bv1 128) ((_ zero_extend 121) (_ bv1 7)))) (_ bv0 128)) (_ bv1 1) (_ bv0 1)))) (let ((?v_30 (bvor ?v_32 (bvnot ?v_29)))) (let ((?v_409 (ite (= (_ bv1 1) ?v_29) (ite (= (_ bv1 1) ?v_30) ?v_408 (bvadd ?v_408 (_ bv1 128))) ?v_408)) (?v_28 (ite (= (bvand x (bvshl (_ bv1 128) ((_ zero_extend 121) (_ bv0 7)))) (_ bv0 128)) (_ bv1 1) (_ bv0 1)))) (not (= (bvnot (ite (= (ite (= (_ bv1 1) (ite (= x (_ bv0 128)) (_ bv1 1) (_ bv0 1))) (_ bv128 128) (bvsub (ite ?v_15 (bvadd ?v_14 (_ bv2 128)) ?v_14) (bvlshr (ite ?v_15 (bvshl ?v_16 ?v_27) ?v_16) ?v_17))) (ite (= (_ bv1 1) ?v_28) (ite (= (_ bv1 1) (bvor ?v_30 (bvnot ?v_28))) ?v_409 (bvadd ?v_409 (_ bv1 128))) ?v_409)) (_ bv1 1) (_ bv0 1))) (_ bv0 1)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
(check-sat)
(exit)
